$\forall$$E$, $A$:Type, $l$:($E$$\rightarrow$$A$), $n$:($A$$\rightarrow$$A$$\rightarrow$$A$), $t$:Tree($E$). t\_iterate($l$;$n$;$t$) $\in$ $A$